Allow zero-sized offsets on dangling pointers in ptr contracts - #625
Merged
feliperodri merged 1 commit intoAug 28, 2026
Merged
Conversation
The requires/ensures clauses of the pointer arithmetic operations
(<*mut T>::{offset,add,sub}, <*const T>::{offset,add,sub},
NonNull::{add,sub}, NonNull::offset_from_unsigned) demanded
same_allocation unconditionally (modulo a ZST escape), although the
documented semantics explicitly permit zero-sized offsets on any
pointer, including dangling ones: "The computed offset, count *
size_of::<T>() bytes, must not overflow isize" and only "if the
computed offset is non-zero, then self must be derived from a pointer
to some allocated object".
The stricter-than-documented clauses are violated by legitimate std
code: slices are allowed to be backed by dangling pointers when empty
(e.g. slice::from_raw_parts(ptr, 0) for arbitrary aligned non-null
ptr), and Iter::new then computes ptr.add(0), and len() computes
end.offset_from_unsigned(begin) on two equal dangling pointers. With
dependency contracts asserted (the Kani default since
model-checking/kani#3802), the slice::iter::verify::verify_tup
harnesses fail on these clauses; evaluating same_allocation on an
allocation-less pointer is additionally a Kani unsupported construct
("Kani does not support reasoning about pointer to unallocated
memory"). The CI configuration currently masks this with
--no-assert-contracts.
Add the documented escape hatches: `count == 0 ||` ahead of the
same-allocation disjunct of offset/add/sub requires and ensures
(matching the precedent already present in NonNull::offset), and an
equal-address escape in NonNull::offset_from_unsigned (matching the
precedent in <*const T>::offset_from).
The unconditional clauses were introduced with the original contracts
in 014965a ("Contracts and Harnesses for `<*mut T>::add`, `sub` and
`offset`" model-checking#113), 688b15b ("Contracts & Harnesses for
`non_null::sub` and `non_null::sub_ptr` and `non_null::offset_from`"
model-checking#93) and siblings.
Verified (Kani 152c6a8c + CBMC 6.10.0):
* slice::iter::verify::verify_tup::{check_next_back_unchecked,
check_advance_back_by} now pass with contracts asserted;
* all 265 proof harnesses matching non_null_check_{add,sub,
offset_from_unsigned} and ptr::verify::check_{mut,const}_{add,sub,
offset} pass both with and without --no-assert-contracts.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
There was a problem hiding this comment.
Pull request overview
This PR updates the formal contracts on core pointer-arithmetic APIs to match the documented Rust semantics that zero-sized offsets are permitted even on dangling pointers, avoiding unnecessary same_allocation requirements that break valid std patterns (e.g., empty slices backed by dangling-but-aligned pointers) when dependency contracts are asserted.
Changes:
- Relax
#[requires]/#[ensures]for*mut T::{offset,add,sub}and*const T::{offset,add,sub}by short-circuiting allocation checks whencount == 0(and preserving the existing ZST escape). - Relax
NonNull::{add,sub}similarly with acount == 0 || size_of::<T>() == 0escape beforesame_allocation. - Relax
NonNull::offset_from_unsignedby allowing equal-address pointers to bypasssame_allocation(zero-sized span), matching the precedent in raw-pointeroffset_from.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| library/core/src/ptr/non_null.rs | Weakens NonNull pointer arithmetic contracts to allow zero offsets / equal-address spans without requiring same_allocation. |
| library/core/src/ptr/mut_ptr.rs | Weakens *mut T offset/add/sub contracts to skip allocation checks when count == 0. |
| library/core/src/ptr/const_ptr.rs | Weakens *const T offset/add/sub contracts to skip allocation checks when count == 0. |
This was referenced Aug 3, 2026
feliperodri
approved these changes
Aug 27, 2026
feliperodri
left a comment
feliperodri
left a comment
Member
There was a problem hiding this comment.
Static review (no local Kani run this time). Adds a count == 0 (plus the existing size_of::<T>() == 0) short-circuit to the same-allocation pre/postconditions of offset/add/sub across const_ptr, mut_ptr and NonNull, and an equal-address short-circuit to NonNull::offset_from. This is a sound precondition relaxation: zero-sized offsets and zero-length spans are always valid per the pointer-method docs, including on dangling pointers such as empty-slice pointers, so the clauses previously rejected inputs that are actually UB-free. The change is identical across the three impls; the mut_ptr and NonNull versions are directly exercised by proof_for_contract.
Minor note: const_ptr's offset/add/sub have no direct proof_for_contract (pre-existing — only offset_from/byte_offset do), so those particular clauses are exercised only transitively / once dependency contracts are asserted; the change is nonetheless sound by inspection and matches the directly-verified mut_ptr/NonNull versions. No concerns.
rajath-mk
approved these changes
Aug 28, 2026
rajath-mk
left a comment
rajath-mk
left a comment
There was a problem hiding this comment.
LGTM. Could take a look at the co pilot comment. But its dated
Merged
via the queue into
model-checking:main
with commit Aug 28, 2026
7b8184c
28 of 29 checks passed
DiuDiu777
pushed a commit
to safer-rust/rapx-verify-rust-std
that referenced
this pull request
Aug 29, 2026
…ing#627) `NonNull::slice_from_raw_parts` is a safe function with no validity requirements on `data`: per its documentation, it is safe to construct the pointer, and only its *use* is subject to safety conditions. Its postcondition however evaluated `unsafe { result.as_ref() }.len()`, creating a reference to the pointed-to memory just to read the slice length — undefined behavior when `data` is dangling or misaligned, and a failing check when the contract is evaluated in such a context. This surfaces with dependency contracts asserted (the Kani default since model-checking/kani#3802): `ptr::non_null::verify::non_null_check_as_uninit_slice_mut` constructs, legitimately, a `NonNull` slice pointer whose span may exceed the backing allocation; evaluating `slice_from_raw_parts`' postcondition then fails with "misaligned pointer to reference cast" / "dereference failure: pointer invalid" inside `NonNull::as_ref`. CI currently masks this with `--no-assert-contracts`. This PR reads the length from the wide-pointer metadata via `NonNull::len` instead, which involves no dereference (and no unsafe code) and is the property the clause is about in the first place. Blame: the dereferencing clause dates to the original contracts in 07318df (model-checking#127). Verified with Kani 152c6a8c + CBMC 6.10.0: `non_null_check_as_uninit_slice_mut`, `non_null_check_slice_from_raw_parts`, `non_null_check_as_uninit_slice` and `non_null_check_len` pass both with and without `--no-assert-contracts` (the first previously failed with contracts asserted — the last remaining failure of that kind known on the 125-harness sample after model-checking#622, model-checking#623, model-checking#624, model-checking#625, model-checking#626). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The requires/ensures clauses of the pointer arithmetic operations (
<*mut T>::{offset,add,sub},<*const T>::{offset,add,sub},NonNull::{add,sub},NonNull::offset_from_unsigned) demandsame_allocationunconditionally (modulo a ZST escape), although the documented semantics explicitly permit zero-sized offsets on any pointer, including dangling ones: only "if the computed offset is non-zero, then self must be derived from a pointer to some allocated object".The stricter-than-documented clauses are violated by legitimate std code: empty slices may be backed by dangling pointers (
slice::from_raw_parts(ptr, 0)for arbitrary aligned non-nullptr— exactly whatslice::iter's ownany_slicehelper generates), whereuponIter::newcomputesptr.add(0)andlen()computesend.offset_from_unsigned(begin)on two equal dangling pointers. With dependency contracts asserted (the Kani default since model-checking/kani#3802), theslice::iter::verify::verify_tupharnesses fail on these clauses — and evaluatingsame_allocationon an allocation-less pointer is additionally a Kani unsupported construct ("Kani does not support reasoning about pointer to unallocated memory"). CI currently masks this via--no-assert-contracts.This PR adds the documented escape hatches:
count == 0 ||ahead of the same-allocation disjunct in offset/add/sub requires and ensures — matching the precedent already present inNonNull::offset— and an equal-address escape inNonNull::offset_from_unsigned, matching the precedent in<*const T>::offset_from.Blame: the unconditional clauses date back to the original contract PRs #113 (014965a) and #93 (688b15b) and siblings.
Verified with Kani 152c6a8c + CBMC 6.10.0:
slice::iter::verify::verify_tup::{check_next_back_unchecked,check_advance_back_by}now pass with contracts asserted;non_null_check_{add,sub,offset_from_unsigned}andptr::verify::check_{mut,const}_{add,sub,offset}pass both with and without--no-assert-contracts.Together with #622, #623, #624 and model-checking/kani#4709/rust-lang#4710, this resolves all verdict differences found on a 125-harness sample when running without
--no-assert-contracts, exceptnon_null_check_from_raw_part_trait(Kani's "unstable vtable comparison 'Eq'" limitation, reached byas_ptr's postcondition on adyn Traitpointee — tracked separately).By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.